It is well-known that the verification of partial correctness properties ofimperative programs can be reduced to the satisfiability problem forconstrained Horn clauses (CHCs). However, state-of-the-art solvers for CHCs(CHC solvers) based on predicate abstraction are sometimes unable to verifysatisfiability because they look for models that are definable in a given classA of constraints, called A-definable models. We introduce a transformationtechnique, called Predicate Pairing (PP), which is able, in many interestingcases, to transform a set of clauses into an equisatisfiable set whosesatisfiability can be proved by finding an A-definable model, and hence can beeffectively verified by CHC solvers. We prove that, under very generalconditions on A, the unfold/fold transformation rules preserve the existence ofan A-definable model, i.e., if the original clauses have an A-definable model,then the transformed clauses have an A-definable model. The converse does nothold in general, and we provide suitable conditions under which the transformedclauses have an A-definable model iff the original ones have an A-definablemodel. Then, we present the PP strategy which guides the application of thetransformation rules with the objective of deriving a set of clauses whosesatisfiability can be proved by looking for A-definable models. PP introduces anew predicate defined by the conjunction of two predicates together with someconstraints. We show through some examples that an A-definable model may existfor the new predicate even if it does not exist for its defining atomicconjuncts. We also present some case studies showing that PP plays a crucialrole in the verification of relational properties of programs (e.g., programequivalence and non-interference). Finally, we perform an experimentalevaluation to assess the effectiveness of PP in increasing the power of CHCsolving.
展开▼
